Inference at * 1 1 0 
Iof proof for Lemma connex functionality wrt iff:



1. T : Type
2. R : TT
3. R' : TT
4. x, y:T. R(x,y)  R'(x,y)
  (x, y:T. R'(x,y)  R'(y,x))  (x, y:T. R'(x,y)  R'(y,x)) 

latex

 by PERMUTE{1:n, 2:n, 3:n, 4:n, 5:n, 1:n, 2:n, 3:n, 4:n, 5:n} 

latex

 1: .....wf..... NILNIL

 1: 5. x, y:T. R'(x,y)  R'(y,x)
 1: 6. x : T
 1: 7. T
 1:   x  T
 2: .....wf..... NILNIL

 2: 5. x, y:T. R'(x,y)  R'(y,x)
 2: 6. T
 2: 7. y : T
 2:   y  T
 3: .....wf..... NILNIL

 3: 5. x, y:T. R'(x,y)  R'(y,x)
 3: 6. T
 3:   T  Type
 4: .....wf..... NILNIL

 4: 5. x, y:T. R'(x,y)  R'(y,x)
 4:   T  Type
 5: .....wf..... NILNIL

 5:   (x, y:T. R'(x,y)  R'(y,x))  
 .

Definitions

f(a), t  T, s = t, x:A  B(x), P  Q, x(s1,s2), , x:AB(x), Type, P  Q, P  Q, P & Q, P  Q, x:A. B(x)